The present disclosure relates to model checking in general, and to bounded model checking using a proof of unsatisfiability provided by a SAT solver, in particular.
Computerized devices control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a testing phase in which the bugs should be discovered. The testing phase is considered one of the most difficult tasks in designing a computerized device. The cost of a bug may be enormous, as its consequences may be disastrous. For example, a bug may cause the injury of a person relying on the designated functionality of the computerized device. Additionally, a bug in hardware or firmware may be expensive to fix, as patching it requires call-back of the computerized device. Hence, many developers of computerized devices invest a substantial portion, such as 70%, of the development cycle to discover erroneous functionalities of the computerized device.
One technique used to find bugs is model checking. A model of the functionality of the computerized device and a set of one or more properties that should be held by the computerized device, also referred to as specification properties, may be utilized by a model checker to determine whether or not the computerized device upholds the specification properties. In some cases, the model represents a possible initial state of the computerized device, and a transition relation function between a state and a next state of the computerized device in a successive timeframe, cycle or other discrete unit representing a phase, generally referred to as a cycle. As the computerized device may operate in an unbounded number of cycles, and as the number of possible states may be large, some model checkers may use abstractions, reductions, symbolic representation of states and other methods to enable model checking of the model. In some cases, a bound on the number of cycles may be utilized, such as to enable proving that the model, and therefore the computerized device, holds the specification property within the bound. Such model checkers are referred to as Bounded Model Checkers (BMCs).
Some BMCs encode a formula representative of a state of the model in all bounded models. An exemplary formula may be
      I    ⋀                  ∏                  i          =                      1.            .            K                              ⁢                          ⁢                        TR          i                ⋀                  ⫬          P                      ,where I is the initial state(s), TRi is a transition relation between state of cycle i−1 and state of cycle i, K is the bound on the number of cycles,
      ∏          i      =              1.        .        K              ⁢          ⁢      TR    i  is a conjunction of all the transition relations between cycle 0 until the bound, and P is the negation of the at least one specification property in respect to variables of state K (also referred to as signals), in respect to variables of all states up to state K, and the like. It is clear that if there exists a state that contradicts the specification property, there will be a satisfying assignment to the formula (i.e., an assignment to all variables of the formula that holds the formula to be TRUE). On the other hand, if the formula is unsatisfiable (i.e., any combination of values to the variables yields the formula to be FALSE), then the bounded model is verified in respect to the specification property.
As is known in the art, a SAT solver may be utilized to determine satisfiability of a formula, such as given in a Conjunctive Normal Form (CNF). For unsatisfiable formulas, the SAT solver may provide a proof of unsatisfiability which comprises of clauses of the CNF (and/or that may be deduced from the CNF) that are already unsatisfiable. A proof of unsatisfiability is a direct acyclic graph. The graph is comprised of a root, intermediate nodes and leaves. The leaves are a portion of the clauses of the CNF. The root of the proof is an empty clause. The intermediate nodes are clauses that are implied by respective parent nodes. For example, an intermediate node may have two parent nodes, from which the intermediate node is obtained by a resolution. An UNSAT core of an unsatisfiable set of clauses is an unsatisfiable subset of theses clauses. An UNSAT core may be determined based on a proof of unsatisfiability, as the proof formally deduces the empty root from a portion of the formula. In this case, the leaves of a proof form an UNSAT core. An UNSAT core may be minimized by iteratively proving unsatisfiability of a previously determined UNSAT core and obtaining a new UNSAT core from the new proof until a fixed-point is reached.
The proof or UNSAT core may be utilized in many model checking related applications, such as for example, in proof-based abstraction-refinement, interpolation and the like.